Inference at * 1 
Iof proof for Lemma bool sq:



1. x : 
2. y : 
3. x = y
  x ~ y 

latex

 by (let T = Unfold `bool` 
in 
in ((((((((((T 1) 
iCollapseTHEN (T 2))) 
iCollapseTHEN (T 3))) 

iCoCollapseTHEN (ApFunToHypEquands `z' case z of inl(x) => x | inr(x) => x Unit 3))) 

iCoCollapseTHENM (ApFunToHypEquands `z' case z of inl(x) => True | inr(x) => False  3))) 

iCoCollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
iC) inil_term)))) 

latex

iC1: 

iC1: 1. x : ?Unit
iC1: 2. y : ?Unit
iC1: 3. x = y
iC1: 4. case x of inl(x) => x | inr(x) => x = case y of inl(x) => x | inr(x) => x
iC1: 5. case x of inl(x) => True | inr(x) => False = case y of inl(x) => True | inr(x) => False
iC1:   x ~ y
iC.

Definitions	, t  T
Lemmas	false wf, true wf, unit wf